(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
*(@x, @y) → #mult(@x, @y)
+(@x, @y) → #add(@x, @y)
appendreverse(@toreverse, @sofar) → appendreverse#1(@toreverse, @sofar)
appendreverse#1(::(@a, @as), @sofar) → appendreverse(@as, ::(@a, @sofar))
appendreverse#1(nil, @sofar) → @sofar
bftMult(@t, @acc) → bftMult'(tuple#2(::(@t, nil), nil), @acc)
bftMult'(@queue, @acc) → bftMult'#1(bftMult'#2(@queue), @acc)
bftMult'#1(tuple#2(@elem, @queue), @acc) → bftMult'#3(@elem, @acc, @queue)
bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) → dequeue(@dequeue@1, @dequeue@2)
bftMult'#3(::(@t, @_@3), @acc, @queue) → bftMult'#4(@t, @acc, @queue)
bftMult'#3(nil, @acc, @queue) → @acc
bftMult'#4(leaf, @acc, @queue) → bftMult'(@queue, @acc)
bftMult'#4(node(@y, @t1, @t2), @acc, @queue) → bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
bftMult'#5(@queue', @acc, @y) → bftMult'(@queue', matrixMult(@acc, @y))
computeLine(@line, @m, @acc) → computeLine#1(@line, @acc, @m)
computeLine#1(::(@x, @xs), @acc, @m) → computeLine#2(@m, @acc, @x, @xs)
computeLine#1(nil, @acc, @m) → @acc
computeLine#2(::(@l, @ls), @acc, @x, @xs) → computeLine(@xs, @ls, lineMult(@x, @l, @acc))
computeLine#2(nil, @acc, @x, @xs) → nil
dequeue(@outq, @inq) → dequeue#1(@outq, @inq)
dequeue#1(::(@t, @ts), @inq) → tuple#2(::(@t, nil), tuple#2(@ts, @inq))
dequeue#1(nil, @inq) → dequeue#2(reverse(@inq))
dequeue#2(::(@t, @ts)) → tuple#2(::(@t, nil), tuple#2(@ts, nil))
dequeue#2(nil) → tuple#2(nil, tuple#2(nil, nil))
enqueue(@t, @queue) → enqueue#1(@queue, @t)
enqueue#1(tuple#2(@outq, @inq), @t) → tuple#2(@outq, ::(@t, @inq))
lineMult(@n, @l1, @l2) → lineMult#1(@l1, @l2, @n)
lineMult#1(::(@x, @xs), @l2, @n) → lineMult#2(@l2, @n, @x, @xs)
lineMult#1(nil, @l2, @n) → nil
lineMult#2(::(@y, @ys), @n, @x, @xs) → ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
lineMult#2(nil, @n, @x, @xs) → ::(*(@x, @n), lineMult(@n, @xs, nil))
matrixMult(@m1, @m2) → matrixMult#1(@m1, @m2)
matrixMult#1(::(@l, @ls), @m2) → ::(computeLine(@l, @m2, nil), matrixMult(@ls, @m2))
matrixMult#1(nil, @m2) → nil
reverse(@xs) → appendreverse(@xs, nil)
The (relative) TRS S consists of the following rules:
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
appendreverse(::(@a430567_6, @as430568_6), @sofar) →+ appendreverse(@as430568_6, ::(@a430567_6, @sofar))
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [@as430568_6 / ::(@a430567_6, @as430568_6)].
The result substitution is [@sofar / ::(@a430567_6, @sofar)].
(2) BOUNDS(n^1, INF)